
module DigitalState

//The projects
sig VoteTime{
initialDate: Int,
endDate: Int,

}

{
//The starts is not before to the end
initialDate<endDate

}
//The projects
sig VoteTimeMember{
initialDate: Int,
endDate: Int,

}
{
//The starts is not before to the end
initialDate<endDate

}

//The users
sig  Citizens{
profile: one Profile
}

//Possible profiles
abstract sig Profile{}

sig GP{
//travels: set Travel
}

sig Member{
citizens:one Citizens
}

//sig Administrator extends Profile{}
sig Candidate {}
//The Package
sig Party{

member:set Member,
candidate:one Candidate


}
{
#candidate=1
}

//Only one Votetime
fact onlyOneVoteTime
{
#VoteTime =1
}
//Only one candidate
fact onlyOneVoteTimeMember
{
#VoteTimeMember =1
}


//************
//Facts
//************
//-------------
//Member facts
//-------------

/*
fact MemberMustHaveACiticen{
all s:Member| some citizen:Citizens | citizen.profile=s
}

//-------------
//candidate facts
//-------------

fact candidateMustHaveAMember{
all p:Candidate| some member:Member | member.profile=p
}
*/
/*
//----------------
//Admnistrator facts
//----------------

//Only one GP
fact onlyOneGP
{
#GP =1
}
//Only one candidate
fact onlyOneCandidate
{
#Candidate =1
}

//An GP must have a system user
fact GPMustHaveOnlyOneUser{
no u1, u2: Member, a:GP | u1!= u2 and u1.profile = u2.profile and u1.profile = a and u2.profile =a
}
*/

//-----------
//party facts
//-----------
/*
fact PartyHasMember
{
all p:member |some g:Party | p in g.member
}
*/


pred show(){

#member > 10
#Party >2

}

run show for 6





